\pagebreak
\appendix

\section{Timings for Zeno and IsaPlanner}
\label{app:timings}

Here we give the list of properties used to compare Zeno and IsaPlanner. The first table (\S \ref{app:sec:one}) gives the properties which both tools could solve, along with the time for each proof. The second table (\S \ref{app:sec:two}) gives the properties which only Zeno could solve and the time it took. The final table (\S \ref{app:sec:three}) gives the properties which neither Zeno nor IsaPlanner could solve. We have omitted ``\li{= True}'' wherever possible for brevity. All the times are in seconds.

\lstset{basicstyle=\ttfamily\scriptsize}

\subsection{Properties both IsaPlanner and Zeno could prove}
\label{app:sec:one}

\scriptsize
\begin{tabular}{c | l | c | c}
\# & \textbf{Property} & Time (Zeno) & Time (IsaPlanner) \\
\hline
1 & \li{concat (take n xs)} \li{(drop n xs)} \li{= xs} & 0.002 & 0.284 \\
2 & \li{add (count n xs)} \li{(count n ys)} \li{= count n (concat xs ys)} & 0.002 & 0.131 \\
3 & \li{leq (count n xs)} \li{(count n (concat xs ys))} & 0.003 & 0.200 \\
4 & \li{add (Suc Zero)} \li{(count n xs)} \li{= count n (Cons n xs)} & 0.001 & 0.086 \\
5 & \li{add (Suc Zero)} \li{(count n xs)} \li{= count n (Cons x xs)} \li{:- eq n x} & 0.000 & 0.132 \\
6 & \li{minus n (add n m)} \li{= Zero} & 0.000 & 0.174 \\
7 & \li{minus (add n m)} \li{n = m} & 0.001 & 0.177 \\
8 & \li{minus (add k m)} \li{(add k n)} \li{= minus m n} & 0.000 & 0.079 \\
9 & \li{minus (minus i j)} \li{k = minus i (add j k)} & 0.002 & 0.270 \\
10 & \li{minus m m = Zero} &  0.000 & 0.068 \\
11 & \li{drop Zero xs = xs} & 0.000 & 0.068 \\
12 & \li{drop n (map f xs)} \li{= map f (drop n xs)} & 0.001 & 0.200 \\
13 & \li{drop (Suc n)} \li{(Cons x xs)} \li{= drop n xs} & 0.000 & 0.073 \\
14 & \li{filter P (concat xs ys)} \li{= concat (filter P xs)} \li{(filter P ys)} & 0.001 & 0.069 \\
15 & \li{len (ins x xs)} \li{= Suc (len xs)} & 0.008 & 0.035 \\
16 & \li{last (Cons x xs)} \li{= x :- x = Nil} & 0.000 & 0.012 \\
17 & \li{leq n Zero = eq n Zero} & 0.000 & 0.065 \\
18 & \li{less i (Suc (add i m))} & 0.000 & 0.251 \\
19 & \li{len (drop n xs)} \li{= minus (len xs)} \li{n} & 0.001 & 0.360 \\
20 & \li{len (sort xs)} \li{= len xs} & 0.038 & 0.047 \\
21 & \li{leq n (add n m)} & 0.000 & 0.168 \\
22 & \li{max (max a b)} \li{c = max a (max b c)} & 0.002 & 0.632 \\
23 & \li{max a b = max b a} & 0.001 & 0.254 \\
24 & \li{eq (max a b)} \li{a = leq b a} & 0.002 & 0.262 \\
25 & \li{eq (max a b)} \li{b = leq a b} & 0.001 & 0.270 \\
26 & \li{mem x (concat xs ys)} \li{:- mem x xs} & 0.017 & 0.069 \\
27 & \li{mem x (concat xs ys)} \li{:- mem x ys} & 0.155 & 0.025 \\
28 & \li{mem x (concat xs (Cons x Nil))} & 0.003 & 0.023 \\
29 & \li{mem x (ins1 x xs)} & 0.002 & 0.027 \\
30 & \li{mem x (ins x xs)} & 0.004 & 0.029 \\
31 & \li{min (min a b)} \li{c = min a (min b c)} & 0.003 & 0.646 \\
32 & \li{min a b = min b a} & 0.001 & 0.259 \\
33 & \li{eq (min a b)} \li{a = leq a b} & 0.000 & 0.265 \\
34 & \li{eq (min a b)} \li{b = leq b a} & 0.001 & 0.261 \\
35 & \li{dropWhile alwaysFalse xs = xs} & 0.000 & 0.011 \\
36 & \li{takeWhile alwaysTrue xs = xs} & 0.000 & 0.009 \\
37 & \li{not (mem x (delete x xs))} & 0.002 & 0.028 \\
38 & \li{count n (concat xs (Cons n Nil))} \li{= Suc (count n xs)} & 0.002 & 0.064 \\
39 & \li{add (count n (Cons x Nil))} \li{(count n xs)} \li{= count n (Cons x xs)} & 0.000 & 0.144 \\
40 & \li{take Zero xs = Nil} & 0.000 & 0.068 \\
41 & \li{take n (map f xs)} \li{= map f (take n xs)} & 0.001 & 0.218 \\
42 & \li{take (Suc n)} \li{(Cons x xs)} \li{= Cons x (take n xs)} & 0.000 & 0.072 \\
43 & \li{concat (takeWhile P xs)} \li{(dropWhile P xs)} \li{= xs} & 0.002 & 0.050 \\
44 & \li{zip (Cons x xs)} \li{ys = zipConcat x xs ys} & 0.001 & 0.222 \\
45 & \li{zip (Cons x xs)} \li{(Cons y ys)} \li{= PCons (Pair x y)} \li{(zip xs ys)} & 0.000 & 0.109 \\
46 & \li{zip Nil ys = PNil} & 0.000 & 0.078 \\
47 & \li{height (mirror a)} \li{= height a} & 0.023 & 0.282 \\
\end{tabular}

\subsection{Properties Zeno alone could prove}
\label{app:sec:two}

\scriptsize
\begin{tabular}{c | l | c}
\# & \textbf{Property} & Time (Zeno) \\
\hline
48 & \li{concat (butlast xs)} \li {(Cons (last xs)} \li {Nil)} \li {= xs :- not (listEq xs Nil)} & 0.002 \\
49 & \li{butlast (concat xs ys)} \li {= butlastConcat xs ys} & 0.003 \\
50 & \li{butlast xs = take (minus (len xs)} \li {(Suc Zero))} \li {xs} & 0.002 \\
51 & \li{butlast (concat xs (Cons x Nil))} \li {= xs} & 0.001 \\
52 & \li{count n xs = count n (rev xs)} & 0.093 \\
53 & \li{count n xs = count n (sort xs)} & 0.136 \\
54 & \li{minus (add m n)} \li {n = m} & 0.004 \\
55 & \li{drop n (concat xs ys)} \li {= concat (drop n xs)} \li {(drop (minus n (len xs))} \li {ys)} & 0.001 \\
56 & \li{drop n (drop m xs)} \li {= drop (add n m)} \li {xs} & 0.008 \\
57 & \li{drop n (take m xs)} \li {= take (minus m n)} \li {(drop n xs)} & 0.014 \\
58 & \li{pdrop n (zip xs ys)} \li {= zip (drop n xs)} \li {(drop n ys)} & 0.006 \\
59 & \li{last (concat xs ys)} \li {= last xs :- ys = Nil} & 0.001 \\
60 & \li{last (concat xs ys)} \li {= last ys :- not (listEq ys Nil)} & 0.024 \\
61 & \li{last (concat xs ys)} \li {= lastOfTwo xs ys} & 0.003 \\
62 & \li{last (Cons x xs)} \li {= last xs :- not (listEq xs Nil)} & 0.000 \\
63 & \li{last (drop n xs)} \li {= last xs :- less n (len xs)} & 0.100 \\
64 & \li{last (concat xs (Cons x Nil))} \li {= x} & 0.001 \\
65 & \li{less i (Suc (add m i))} & 0.001 \\
66 & \li{len (butlast xs)} \li {= minus (len xs)} \li {(Suc Zero)} & 0.001 \\
67 & \li{leq n (add m n)} & 0.006 \\
68 & \li{rev (filter P xs)} \li {= filter P (rev xs)} & 0.010 \\
69 & \li{count n (concat xs (Cons m Nil))} \li {= count n xs :- not (eq n m)} & 0.003 \\
70 & \li{add (count n xs)} \li {(count n (Cons m Nil))} \li {= count n (Cons m xs)} & 0.007 \\
71 & \li{minus (minus (Suc m)} \li {n)} \li {(Suc k)} \li {= minus (minus m n)} \li {k} & 0.002 \\
72 & \li{take n (concat xs ys)} \li {= concat (take n xs)} \li {(take (minus n (len xs))} \li {ys)} & 0.001 \\
73 & \li{take n (drop m xs)} \li {= drop m (take (add n m)} \li {xs)} & 0.013 \\
74 & \li{ptake n (zip xs ys)} \li {= zip (take n xs)} \li {(take n ys)} & 0.004 \\
75 & \li{zip (concat xs ys)} \li {zs =} \\
& \hspace{20pt} \li{pconcat (zip xs (take (len xs)} \li {zs))} \li {(zip ys (drop (len xs)} \li {zs))} & 0.011 \\
76 & \li{zip xs (concat ys zs)} \li {=} \\
& \hspace{20pt} \li{pconcat (zip (take (len ys)} \li {xs)} \li {ys)} \li {(zip (drop (len ys)} \li {xs)} \li {zs)} & 0.003 \\
\end{tabular}

\subsection{Properties neither tool could prove}
\label{app:sec:three}

\scriptsize
\begin{tabular}{c | l}
\# & \textbf{Property} \\
\hline
77 & \li{leq (len (filter P xs))} \li{(len xs)} \\
78 & \li{leq (len (delete n xs))} \li{(len xs)} \\
79 & \li{mem x (ins y xs)} \li{= mem x xs :- not (eq x y)} \\
80 & \li{rev (drop i xs)} \li{= take (minus (len xs)} \li{i)} \li{(rev xs)} \\
81 & \li{rev (take i xs)} \li{= drop (minus (len xs)} \li{i)} \li{(rev xs)} \\
82 & \li{sorted (insort x xs)} \li{:- sorted xs} \\
83 & \li{sorted (sort xs)} \\
84 & \li{zip (rev xs)} \li{(rev ys)} \li{= prev (zip xs ys)} \li{:- len xs = len ys}
\end{tabular}

\normalsize

\section{Haskell code for the test suite}
\label{app:code}

\lstset{basicstyle=\ttfamily\footnotesize}

\begin{lstlisting}
module Comparison where

import Prelude ()

-- Boolean datatype
data Bool = True | False

-- Natural numbers
data Nat  = Zero | Suc Nat

-- List of natural numbers
data List = Nil  | Cons Nat List

-- Pair (2-tuple) of natural numbers
data Pair = Pair Nat Nat

-- List of pairs of natural numbers
data PList = PNil | PCons Pair PList

-- Binary tree of natural numbers
data Tree = Leaf | Node Tree Nat Tree


-- Boolean functions

not :: Bool -> Bool
not True = False
not False = True

and :: Bool -> Bool -> Bool
and True True = True
and _ _ = False


-- Natural number functions

add :: Nat -> Nat -> Nat
add Zero y = y
add (Suc x) y = Suc (add x y)

minus :: Nat -> Nat -> Nat
minus Zero _ = Zero
minus x Zero = x
minus (Suc x) (Suc y) = minus x y 

mul :: Nat -> Nat -> Nat
mul Zero _ = Zero
mul (Suc x) y = add y (mul x y)

eq :: Nat -> Nat -> Bool
eq Zero Zero = True
eq Zero _ = False
eq (Suc _) Zero = False
eq (Suc x) (Suc y) = eq x y

leq :: Nat -> Nat -> Bool
leq Zero _ = True
leq (Suc x) Zero = False
leq (Suc x) (Suc y) = leq x y

less :: Nat -> Nat -> Bool
less _ Zero = False
less Zero _ = True
less (Suc x) (Suc y) = less x y

min :: Nat -> Nat -> Nat
min Zero y = Zero
min (Suc x) Zero = Zero
min (Suc x) (Suc y) = Suc (min x y)

max :: Nat -> Nat -> Nat
max Zero y = y
max x Zero = x
max (Suc x) (Suc y) = Suc (max x y)

alwaysTrue :: Nat -> Bool
alwaysTrue _ = True

alwaysFalse :: Nat -> Bool
alwaysFalse _ = False


-- List functions

null :: List -> Bool
null Nil = True
null _ = False

listEq :: List -> List -> Bool
listEq Nil Nil = True
listEq (Cons _ _) Nil = False
listEq Nil (Cons _ _) = False
listEq (Cons x xs) (Cons y ys) = 
  (x `eq` y) `and` (xs `listEq` ys)

concat :: List -> List -> List
concat Nil ys = ys
concat (Cons x xs) ys = Cons x (concat xs ys)

rev :: List -> List
rev Nil = Nil
rev (Cons x xs) = concat (rev xs) (Cons x Nil)
    
mem :: Nat -> List -> Bool
mem _ Nil = False
mem n (Cons x xs) = 
  case n `eq` x of
    True -> True
    False -> mem n xs
    
delete :: Nat -> List -> List
delete _ Nil = Nil
delete n (Cons x xs) = 
  case n `eq` x of
    True -> delete n xs
    False -> Cons x (delete n xs)
    
drop :: Nat -> List -> List
drop Zero xs = xs
drop _ Nil = Nil
drop (Suc x) (Cons _ xs) = drop x xs

take :: Nat -> List -> List
take Zero _ = Nil
take _ Nil = Nil
take (Suc x) (Cons y ys) = Cons y (take x ys) 

len :: List -> Nat
len Nil = Zero
len (Cons _ xs) = Suc (len xs)

count :: Nat -> List -> Nat
count x Nil = Zero
count x (Cons y ys) =
  case x `eq` y of
    True -> Suc (count x ys)
    False -> count x ys

butlast :: List -> List
butlast Nil = Nil
butlast (Cons x Nil) = Nil
butlast (Cons x xs) = Cons x (butlast xs)

last :: List -> Nat
last Nil = Zero
last (Cons x Nil) = x
last (Cons x xs) = last xs

map :: (Nat -> Nat) -> List -> List
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)

takeWhile :: (Nat -> Bool) -> List -> List
takeWhile _ Nil = Nil
takeWhile p (Cons x xs) = 
  case p x of
    True -> Cons x (takeWhile p xs)
    False -> Nil
    
dropWhile :: (Nat -> Bool) -> List -> List
dropWhile _ Nil = Nil
dropWhile p (Cons x xs) =
  case p x of
    True -> dropWhile p xs
    False -> Cons x xs
    
filter :: (Nat -> Bool) -> List -> List
filter _ Nil = Nil
filter p (Cons x xs) = 
  case p x of
    True -> Cons x (filter p xs)
    False -> filter p xs
    
sorted :: List -> Bool
sorted Nil = True
sorted (Cons x Nil) = True
sorted (Cons x (Cons y ys)) = 
  case x `leq` y of
    False -> False
    True -> sorted (Cons y ys)
    
insort :: Nat -> List -> List
insort x Nil = Cons x Nil
insort x (Cons y ys) =
  case x `leq` y of
    True -> Cons x (Cons y ys)
    False -> Cons y (insort x ys)
    
ins :: Nat -> List -> List
ins n Nil = Cons n Nil
ins n (Cons x xs) =
  case n `less` x of
    True -> Cons n (Cons x xs)
    False -> Cons x (ins n xs)
    
ins1 :: Nat -> List -> List
ins1 n Nil = Cons n Nil
ins1 n (Cons x xs) = 
  case n `eq` x of
    True -> Cons x xs
    False -> Cons x (ins1 n xs)
        
sort :: List -> List
sort Nil = Nil
sort (Cons x xs) = insort x (sort xs)

butlastConcat :: List -> List -> List
butlastConcat xs Nil = butlast xs
butlastConcat xs ys = xs `concat` butlast ys

lastOfTwo :: List -> List -> Nat
lastOfTwo xs Nil = last xs
lastOfTwo _ ys = last ys 

-- Pair list functions

zip :: List -> List -> PList
zip Nil _ = PNil
zip _ Nil = PNil
zip (Cons x xs) (Cons y ys) = PCons (Pair x y) (zip xs ys)

zipConcat :: Nat -> List -> List -> PList
zipConcat _ _ Nil = PNil
zipConcat x xs (Cons y ys) = PCons (Pair x y) (zip xs ys) 

pdrop :: Nat -> PList -> PList
pdrop Zero xs = xs
pdrop _ PNil = PNil
pdrop (Suc n) (PCons _ xs) = pdrop n xs

ptake :: Nat -> PList -> PList
ptake Zero _ = PNil
ptake _ PNil = PNil
ptake (Suc n) (PCons x xs) = PCons x (ptake n xs)

pconcat :: PList -> PList -> PList
pconcat PNil ys = ys
pconcat (PCons x xs) ys = PCons x (pconcat xs ys)


-- Binary tree functions

height :: Tree -> Nat
height Leaf = Zero
height (Node l x r) = Suc (max (height l) (height r))

mirror :: Tree -> Tree
mirror Leaf = Leaf
mirror (Node l x r) = Node (mirror r) x (mirror l)
\end{lstlisting}